package automatica.upgrade;

import java.io.File;
import java.io.IOException;
import java.util.Vector;

import javax.swing.JOptionPane;

import prefuse.data.Table;
import ui.Utility;

public class TheoremGenerater {
	
	public TheoremGenerater(String path){
		try {
			String content = Utility.readFile(path);
			int d = path.lastIndexOf("/")==-1?path.lastIndexOf("\\")+1:path.lastIndexOf("/")+1;
			if(d!=-1&&d!=0){
				name = path.substring(d, path.lastIndexOf("."));
			}
			this.initialize(content);
			this.print();
			
			this.simplify();
			this.print();
			
			this.generateTheorem();
			//this.print();
			
			this.packageTheorem(path);
			
		} catch (IOException e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		}
		
	}
	
	private void initialize(String content){
		//generate a table to store the information of the content
		objectTable.addColumn("role", int.class);
		objectTable.addColumn("reference", String.class);
		objectTable.addColumn("vocabulary", String.class);
		objectTable.addColumn("attribute1", String.class);
		objectTable.addColumn("attribute2", String.class);
		objectTable.addColumn("geobject", String.class);
		objectTable.addColumn("count", int.class);
		
		constraintTable.addColumn("role", int.class);
		constraintTable.addColumn("reference", String.class);
		constraintTable.addColumn("vocabulary", String.class);
		constraintTable.addColumn("attribute1", String.class);
		constraintTable.addColumn("attribute2", String.class);
		constraintTable.addColumn("geobject", String.class);
		Vector<String> list = Utility.getItemsBySeparator(content, "\n");
		for(int i = 0; i < list.size(); i++){
			String currentItem = list.get(i);
			int s = currentItem.indexOf("=");
			//A=...
			if(s!=-1){
				objectTable.addRow();
				int currentIndex = objectTable.getRowCount()-1;
				objectTable.setString(currentIndex, "reference", currentItem.substring(0,s));
				String str = currentItem.substring(s+1,currentItem.length());
				if(str.trim().startsWith("(")){
					objectTable.setString(currentIndex, "vocabulary", "point");
					objectTable.setInt(currentIndex, "role", 1);
					objectTable.setString(currentIndex, "geobject", str);
					objectTable.setInt(currentIndex,"count",0);
				}else{
					Vector<String> items = Utility.generateTermSet(str);
					objectTable.setString(currentIndex, "vocabulary", items.get(0));
					objectTable.setString(currentIndex, "attribute1", items.get(1));
					objectTable.setString(currentIndex, "attribute2", items.get(2));
					objectTable.setInt(currentIndex, "role", 0);
					objectTable.setString(currentIndex, "geobject", str);
				}
			}else{
				constraintTable.addRow();
				int currentIndex = constraintTable.getRowCount()-1;
				Vector<String> items = Utility.generateTermSet(currentItem);
				if(items.size()==3){
					constraintTable.setString(currentIndex, "vocabulary", items.get(0));
					constraintTable.setString(currentIndex, "attribute1", items.get(1));
					constraintTable.setString(currentIndex, "attribute2", items.get(2));
					constraintTable.setInt(currentIndex, "role", 1);
					//constraintTable.setString(currentIndex, "geobject", currentItem);
				}else{
					JOptionPane.showMessageDialog(null,"The item has more than 2 attributes.","",JOptionPane.ERROR_MESSAGE);
				}
			}
		}

	}
	

	private void print(){
		System.out.println("role------reference------vocabulary------attribute1------attribute2------geobject------count");
		for(int i = 0; i < objectTable.getRowCount(); i++){
			System.out.println(objectTable.getInt(i, "role")+"----"+objectTable.getString(i, "reference")+"----"
					+objectTable.getString(i, "vocabulary")+"----"+objectTable.getString(i, "attribute1")+"----"+objectTable.getString(i, "attribute2")+"----"+objectTable.getString(i, "geobject")+"----"+objectTable.getInt(i, "count"));
		}	
		System.out.println("role------reference------vocabulary------attribute1------attribute2------geobject");
		for(int i = 0; i < constraintTable.getRowCount(); i++){
			System.out.println(constraintTable.getInt(i, "role")+"----"+constraintTable.getString(i, "reference")+"----"
					+constraintTable.getString(i, "vocabulary")+"----"+constraintTable.getString(i, "attribute1")+"----"+constraintTable.getString(i, "attribute2")+"----"+constraintTable.getString(i, "geobject"));
		}	
	}
	
	private void simplify(){
		
		countOccurence();
		
		reasoning();
		
		generateObjects();

	}
	
	private void generateTheorem(){
		Vector<String> constraints = new Vector<String>(1,1);
		Vector<String> objects = new Vector<String>(1,1);
		for(int i = 0 ; i < constraintTable.getRowCount(); i++){
			if(constraintTable.getInt(i, "role")==1){
				String str = constraintTable.getString(i, "vocabulary").replace(incidentCircle, "incident")+"("+constraintTable.getString(i, "attribute1")+","+constraintTable.getString(i, "attribute2")+")";
				constraintTable.setString(i, "geobject", str);
				constraints.add(str);
			}
		}
		
		for(int i = 0 ; i < objectTable.getRowCount(); i++){
			if(objectTable.getInt(i, "role")==1){
				String str = objectTable.getString(i, "reference")+":=point()";
				objects.add(str);
			}
		}
		
		//Each constraint determines a theorem
		for(int t = 0 ; t < constraints.size(); t++){
			StringBuffer theorem = new StringBuffer(1);
			theorem.append("Problem(" + name +(t+1)+",Theorem,assume(");
			for(int k = 0; k < objects.size(); k++){
				theorem.append(objects.get(k)+",");
			}
			for(int l = 0; l < constraints.size(); l++){
				if(l!=t){
					theorem.append(constraints.get(l)+",");
				}
			}
			theorem.replace(theorem.lastIndexOf(","), theorem.length(), "),show("+constraints.get(t)+"))");
			if(filterTheorem(theorem.toString())!=null){
				theorems.add(theorem.toString());
			}
		}
		
	}
	
	private String filterTheorem(String theorem){
		//use algebraic computation and numerical computation to test the truth of a theorem
		String result = theorem;
		
		//heuristic rules for ordering predicates
		
		
		//determine arbitrary points for the theorem
		
		
		//assign coordinates and compute triangular set
		
		
		//assign random values in u and determine the values of other coordinates
		
		
		//check whether the conclusion holds. If not, kick off the theorem from candidates
		
		
		return result;
		
	}
	
	
	private void packageTheorem(String path){
		StringBuffer output = new StringBuffer(1);
		output.append("Problems(");
		for(int i = 0; i < theorems.size(); i++){
			//System.out.println(theorems.get(i));
			output.append(theorems.get(i)+",");
		}output.replace(output.lastIndexOf(","), output.length(), ")");
		
		Utility.saveFile(null, output.toString(), new File(path.replace(".txt", "Theorems.txt")));
	}
	
	
	private void countOccurenceFromFunction(String obj){
		if(obj.indexOf("(")!=-1){
			Vector<String> v = Utility.generateTermSet(obj);
			for(int p = 1; p < v.size(); p++){
				countOccurenceFromFunction(v.get(p));
			}
		}else{
			int objectRowNum = automatica.Utility.getRowNum(objectTable,obj,"reference");
			if(objectRowNum!=-1){
				objectTable.setInt(objectRowNum, "count", objectTable.getInt(objectRowNum, "count")+1);
			}
		}
	}
	
	private void countOccurence(){
		for(int i = 0; i < objectTable.getRowCount();i++){	
			objectTable.setInt(i, "count", 0);
		}
		//count the occurence
		for(int i = 0; i < constraintTable.getRowCount();i++){
			//suppose that the constraints are binary relations
			String attr1 = constraintTable.getString(i, "attribute1");
			String attr2 = constraintTable.getString(i, "attribute2");
			int attr1RowNum = automatica.Utility.getRowNum(objectTable,attr1,"reference");
			int attr2RowNum = automatica.Utility.getRowNum(objectTable,attr2,"reference");
			
			//deal with relation of incident
			if(constraintTable.getString(i, "vocabulary").equals("incident")){
				if(attr1RowNum!=-1){
					objectTable.setInt(attr1RowNum, "count", objectTable.getInt(attr1RowNum, "count")+1);
				}
				if(attr2RowNum!=-1){
					//check whether it is the case incident(A,line(A,B))
					//if(attr1.equals(objectTable.getString(attr2RowNum, "attribute1"))||attr1.equals(objectTable.getString(attr2RowNum, "attribute2"))){
						//constraintTable.setInt(i, "role", 0);
					//}else{		
						//count the occurence times of labels
						String obj = objectTable.getString(attr2RowNum, "geobject");
						countOccurenceFromFunction(obj);
						//constraintTable.setString(i, "attribute2", obj);
					//}
				}
			}else
				if(constraintTable.getString(i, "vocabulary").equals("pointOnC")||constraintTable.getString(i, "vocabulary").equals("incidentCircle")){
					if(attr1RowNum!=-1){
						objectTable.setInt(attr1RowNum, "count", objectTable.getInt(attr1RowNum, "count")+1);
					}
					if(attr2RowNum!=-1){
						String obj = objectTable.getString(attr2RowNum, "geobject");
						countOccurenceFromFunction(obj);
					}
						
				}else
					if(constraintTable.getString(i, "vocabulary").equals("perpendicular")||constraintTable.getString(i, "vocabulary").equals("parallel")){
						if(attr1RowNum!=-1){
							String obj = objectTable.getString(attr1RowNum, "geobject");
							//constraintTable.setString(i, "attribute1", obj);		
							countOccurenceFromFunction(obj);
						}
						if(attr2RowNum!=-1){
							String obj = objectTable.getString(attr2RowNum, "geobject");
							//constraintTable.setString(i, "attribute2", obj);
							countOccurenceFromFunction(obj);
						}
					}else
						if(constraintTable.getString(i, "vocabulary").equals("equal")){
							if(attr1RowNum==-1){
								countOccurenceFromFunction(attr1);
							}
							if(attr2RowNum==-1){
								countOccurenceFromFunction(attr2);
							}
						}
		}
	}
	
	
	private void reasoning(){
		print();
		//remove redundant incidences: incident(A,l) and incident(B,l)
		for(int k = 0; k < constraintTable.getRowCount(); k++){
			if(constraintTable.getInt(k, "role") > 0){
				if(constraintTable.getString(k, "vocabulary").equals("incident")){
					String objLabel = constraintTable.getString(k, "attribute2");
					for(int j = k+1; j < constraintTable.getRowCount(); j++){
						String newStr = null;
						if(objLabel.equals(constraintTable.getString(j, "attribute2"))&&constraintTable.getInt(j, "role")>0){
							String label1 = constraintTable.getString(k, "attribute1");
							String label2 = constraintTable.getString(j, "attribute1");
							int row1 = automatica.Utility.getRowNum(objectTable,label1,"reference");
							int row2 = automatica.Utility.getRowNum(objectTable,label2,"reference");		
							int buf = automatica.Utility.getRowNum(objectTable,objLabel,"reference");
							String label3 = objectTable.getString(buf, "attribute1");
							String label4 = objectTable.getString(buf, "attribute2");
							int row3 = automatica.Utility.getRowNum(objectTable,label3,"reference");
							int row4 = automatica.Utility.getRowNum(objectTable,label4,"reference");
	
							int count1 = objectTable.getInt(row1, "count");
							int count2 = objectTable.getInt(row2, "count");
							int count3 = objectTable.getInt(row3, "count");
							int count4 = objectTable.getInt(row4, "count");
							
							//determine while label should be eliminated
							if(count3<=count4){
								if((count3 <= count1 || count3 <= count2)){
									if(count1 <= count2){
										int flag = 0;
										//check whether it will be incident(A,line(A,B))
										if(!label3.equals(label2) && !label4.equals(label2)){
											objectTable.setString(buf, "attribute1", label2);
											newStr = objectTable.getString(buf, "geobject").replace("("+label3+",", "("+label2+",");
											objectTable.setString(buf, "geobject", newStr);
											constraintTable.setInt(j, "role", 0);
											flag++;
											//reset the occurence times
											countOccurence();
										}
										
										if(count4 <= count1){
											if(!label3.equals(label1) && !label4.equals(label1)){
												objectTable.setString(buf, "attribute2", label1);
												newStr = objectTable.getString(buf, "geobject").replace(","+label4+")", ","+label1+")");
												objectTable.setString(buf, "geobject", newStr);
												constraintTable.setInt(k, "role", 0);
												flag++;
												countOccurence();
											}
										}
										//if two attributes are replaced, then break
										if(flag == 2){
											break;
										}

									}else{
										int flag = 0;
										if(!label3.equals(label1) && !label4.equals(label1)){
											objectTable.setString(buf, "attribute1", label1);
											newStr = objectTable.getString(buf, "geobject").replace("("+label3+",", "("+label1+",");
											objectTable.setString(buf, "geobject", newStr);
											constraintTable.setInt(k, "role", 0);
											flag++;
											//reset the occurence times
											countOccurence();
										}
										
										if(count4 <= count2){
											if(!label3.equals(label2) && !label4.equals(label2)){
												objectTable.setString(buf, "attribute2", label2);
												newStr = objectTable.getString(buf, "geobject").replace(","+label4+")", ","+label2+")");
												objectTable.setString(buf, "geobject", newStr);
												constraintTable.setInt(j, "role", 0);
												flag++;
												//reset the occurence times
												countOccurence();
											}
										}
										
										//if two attributes are replaced, then break
										if(flag == 2){
											break;
										}
									}
								}
							}else{
								if((count4 <= count1 || count4 <= count2)){
									if(count1 <= count2){
										int flag = 0;
										if(!label3.equals(label2) && !label4.equals(label2)){
											objectTable.setString(buf, "attribute2", label2);
											newStr = objectTable.getString(buf, "geobject").replace(","+label4+")", ","+label2+")");
											objectTable.setString(buf, "geobject", newStr);
											constraintTable.setInt(j, "role", 0);
											flag++;
											//reset the occurence times
											countOccurence();
										}
										
										if(count3 <= count1){
											if(!label3.equals(label1) && !label4.equals(label1)){
												objectTable.setString(buf, "attribute1", label1);
												newStr = objectTable.getString(buf, "geobject").replace("("+label3+",", "("+label1+",");
												objectTable.setString(buf, "geobject", newStr);
												constraintTable.setInt(k, "role", 0);
												flag++;
												//reset the occurence times
												countOccurence();
											}
										}
										
										//if two attributes are replaced, then break
										if(flag == 2){
											break;
										}

									}else{
										int flag = 0;
										if(!label3.equals(label1) && !label4.equals(label1)){
											objectTable.setString(buf, "attribute2", label1);
											newStr = objectTable.getString(buf, "geobject").replace(","+label4+")", ","+label1+")");
											objectTable.setString(buf, "geobject", newStr);
											constraintTable.setInt(k, "role", 0);
											flag++;
											//reset the occurence times
											countOccurence();
										}
										
										if(count3 <= count2){
											if(!label3.equals(label2) && !label4.equals(label2)){
												objectTable.setString(buf, "attribute1", label2);
												newStr = objectTable.getString(buf, "geobject").replace("("+label3+",", "("+label2+",");
												objectTable.setString(buf, "geobject", newStr);
												constraintTable.setInt(j, "role", 0);
												flag++;
												//reset the occurence times
												countOccurence();
											}
										}
										//if two attributes are replaced, then break
										if(flag == 2){
											break;
										}
									}
								}
							}
						}
					}
				}else
					if(constraintTable.getString(k, "vocabulary").equals("pointOnC")){
						String objLabel = constraintTable.getString(k, "attribute2");
						Vector<String> labels = new Vector<String>(1,1);
						Vector<Integer> objectRows = new Vector<Integer>(1,1);
						labels.add(constraintTable.getString(k, "attribute1"));
						objectRows.add(k);
						for(int j = k+1; j < constraintTable.getRowCount(); j++){
							if(objLabel.equals(constraintTable.getString(j, "attribute2"))&&constraintTable.getInt(j,"role")>0){
								labels.add(constraintTable.getString(j, "attribute1"));
								objectRows.add(j);
								System.out.println("Label: " + constraintTable.getString(j, "attribute1"));
							}
						}
						System.out.println("Labelsize: " + labels.size());
						
						if(labels.size()==1){
							//the circle is redundant
							constraintTable.setInt(k, "role", 0);
						}else
							if(labels.size()==2){
								int row1 = automatica.Utility.getRowNum(objectTable,labels.get(0),"reference");
								int row2 = automatica.Utility.getRowNum(objectTable,labels.get(1),"reference");
								int objRow = automatica.Utility.getRowNum(objectTable,objLabel,"geobject");
								int count1 = objectTable.getInt(row1, "count");
								int count2 = objectTable.getInt(row2, "count");
								if(count1 <= count2){
									String length = objectTable.getString(objRow, "attribute2");
									String newObj = objectTable.getString(objRow, "geobject").replace(length, labels.get(1));
									objectTable.setString(objRow, "attribute2", labels.get(1));
									objectTable.setString(objRow, "geobject", newObj);
									constraintTable.setInt(row2, "role", 0);
								}else{
									String length = objectTable.getString(objRow, "attribute2");
									String newObj = objectTable.getString(objRow, "geobject").replace(length, labels.get(0));
									objectTable.setString(objRow, "attribute2", labels.get(0));
									objectTable.setString(objRow, "geobject", newObj);
									constraintTable.setInt(row1, "role", 0);
								}
							}else
								if(labels.size()>=3){
									//select the first three labels with most counts
									Vector<Integer> labelCounts = new Vector<Integer>(1,1);
									for(int m = 0; m < labels.size(); m++){
										labelCounts.add(objectTable.getInt(automatica.Utility.getRowNum(objectTable,labels.get(m),"reference"), "count"));
										System.out.println("Counts:" + labelCounts.get(m));
									}
									int[] a = new int[3];
									a[0] = 0;
									for(int p = 1; p < labelCounts.size(); p++){
										if(labelCounts.get(p) > labelCounts.get(a[0])){
											a[0] = p;
										}
									}
									labelCounts.set(a[0], 0);
									a[1] = 0;
									for(int p = 1; p < labelCounts.size(); p++){
										if(labelCounts.get(p) > labelCounts.get(a[1])){
											a[1] = p;
										}
									}
									labelCounts.set(a[1],0);
									a[2] = 0;
									for(int p = 1; p < labelCounts.size(); p++){
										if(labelCounts.get(p) > labelCounts.get(a[2])){
											a[2] = p;
										}
									}
									
									//replace the circle object
									int objRow = automatica.Utility.getRowNum(objectTable,objLabel,"reference");
									objectTable.setString(objRow, "geobject", "circle("+labels.get(a[0])+","+labels.get(a[1])+","+labels.get(a[2])+")");
									String center = objectTable.getString(objRow, "attribute1");
									
									//set the role with 0
									constraintTable.setInt(objectRows.get(a[0]), "role", 0);
									constraintTable.setInt(objectRows.get(a[1]), "role", 0);
									constraintTable.setInt(objectRows.get(a[2]), "role", 0);
									
									for(int t = 0; t < objectRows.size(); t++){
										if(t!=a[0]&&t!=a[1]&&t!=a[2]){
											constraintTable.setString(objectRows.get(t), "vocabulary", incidentCircle);
										}
									}
									
									//recover the information of center of the circle
									constraintTable.addRow();
									int current = constraintTable.getRowCount()-1;
									constraintTable.set(current, "role", 1);
									constraintTable.set(current, "vocabulary", "equal");
									constraintTable.set(current, "attribute1", "distance("+center+","+labels.get(a[0])+")");
									constraintTable.set(current, "attribute2", "distance("+center+","+labels.get(a[1])+")");
									
								}
						countOccurence();
					}
			}
		}
		
		
		//check whether incident(A,line(A,B))
		for(int i = 0; i < constraintTable.getRowCount();i++){
			//suppose that the constraints are binary relations
			String attr1 = constraintTable.getString(i, "attribute1");
			String attr2 = constraintTable.getString(i, "attribute2");
			int attr1RowNum = automatica.Utility.getRowNum(objectTable,attr1,"reference");
			int attr2RowNum = automatica.Utility.getRowNum(objectTable,attr2,"reference");
			
			//deal with relation of incident
			if(constraintTable.getString(i, "vocabulary").equals("incident")){
				if(attr2RowNum!=-1){
					//check whether it is the case incident(A,line(A,B))
					if(attr1.equals(objectTable.getString(attr2RowNum, "attribute1"))||attr1.equals(objectTable.getString(attr2RowNum, "attribute2"))){
						constraintTable.setInt(i, "role", 0);
					}
				}
			}
		}
		
	}
	
	private void generateObjects(){
		//simplify object table
		//if the count number of a point is less than threshold, then the point is useless; otherwise, the point is useful. 
		for(int i = 0; i < objectTable.getRowCount(); i++){
			if(objectTable.getInt(i, "count") < threshold && objectTable.getString(i, "vocabulary").equals("point")){
				objectTable.setInt(i, "role", 0);
				String redundantReference = objectTable.getString(i, "reference");
				for(int j = 0 ; j < constraintTable.getRowCount(); j++){
					String attr1 = constraintTable.getString(j, "attribute1");
					if(attr1.equals(redundantReference)||attr1.indexOf(redundantReference+",")!=-1||attr1.indexOf(","+redundantReference)!=-1){
						constraintTable.setInt(j,"role",0);
					}
					String attr2 = constraintTable.getString(j, "attribute2");
					if(attr2.equals(redundantReference)||attr2.indexOf(redundantReference+",")!=-1||attr2.indexOf(","+redundantReference)!=-1){
						constraintTable.setInt(j,"role",0);
					}
				}
			}
		}
		
		for(int t = 0; t < constraintTable.getRowCount(); t++){
			if(constraintTable.getInt(t,"role")!=0){
				int row1 = automatica.Utility.getRowNum(objectTable,constraintTable.getString(t, "attribute1"),"reference");
				if(row1!=-1&&!objectTable.getString(row1, "geobject").startsWith("(")){
					constraintTable.set(t, "attribute1", objectTable.getString(row1, "geobject"));
				}
				int row2 = automatica.Utility.getRowNum(objectTable,constraintTable.getString(t, "attribute2"),"reference");
				if(row2!=-1&&!objectTable.getString(row2, "geobject").startsWith("(")){
					constraintTable.set(t, "attribute2", objectTable.getString(row2, "geobject"));
				}
			}			
		}
	}
	
	
	private Table objectTable = new Table();
	private Table constraintTable = new Table();
	private Vector<String> theorems = new Vector<String>(1,1);
	private String name = "Proposition";
	private int threshold = 3;
	private String incidentCircle = "incidentCircle";

}
